Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(F1, Gs)), NF)
REDUCE'II'IN2(sequent2(nil, nil), sequent2(F1, F2)) -> U'15'11(intersect'ii'in2(F1, F2))
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
INTERSECT'II'IN2(Xs, cons2(X0, Ys)) -> U'1'11(intersect'ii'in2(Xs, Ys))
REDUCE'II'IN2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> U'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> U'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> U'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> U'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right))
REDUCE'II'IN2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> U'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> U'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> U'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
INTERSECT'II'IN2(Xs, cons2(X0, Ys)) -> INTERSECT'II'IN2(Xs, Ys)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> U'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> U'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(nil, nil), sequent2(F1, F2)) -> INTERSECT'II'IN2(F1, F2)
REDUCE'II'IN2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right)))
REDUCE'II'IN2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> U'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
INTERSECT'II'IN2(cons2(X0, Xs), Ys) -> U'2'11(intersect'ii'in2(Xs, Ys))
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> REDUCE'II'IN2(sequent2(cons2(G1, Fs), Gs), NF)
INTERSECT'II'IN2(cons2(X0, Xs), Ys) -> INTERSECT'II'IN2(Xs, Ys)
REDUCE'II'IN2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> U'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
TAUTOLOGY'I'IN1(F) -> REDUCE'II'IN2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil))
REDUCE'II'IN2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> U'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
REDUCE'II'IN2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF)
TAUTOLOGY'I'IN1(F) -> U'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(F1, Gs)), NF)
REDUCE'II'IN2(sequent2(nil, nil), sequent2(F1, F2)) -> U'15'11(intersect'ii'in2(F1, F2))
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
INTERSECT'II'IN2(Xs, cons2(X0, Ys)) -> U'1'11(intersect'ii'in2(Xs, Ys))
REDUCE'II'IN2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> U'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> U'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> U'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> U'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right))
REDUCE'II'IN2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> U'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> U'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> U'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
INTERSECT'II'IN2(Xs, cons2(X0, Ys)) -> INTERSECT'II'IN2(Xs, Ys)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> U'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> U'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(nil, nil), sequent2(F1, F2)) -> INTERSECT'II'IN2(F1, F2)
REDUCE'II'IN2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right)))
REDUCE'II'IN2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> U'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
INTERSECT'II'IN2(cons2(X0, Xs), Ys) -> U'2'11(intersect'ii'in2(Xs, Ys))
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> REDUCE'II'IN2(sequent2(cons2(G1, Fs), Gs), NF)
INTERSECT'II'IN2(cons2(X0, Xs), Ys) -> INTERSECT'II'IN2(Xs, Ys)
REDUCE'II'IN2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> U'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
TAUTOLOGY'I'IN1(F) -> REDUCE'II'IN2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil))
REDUCE'II'IN2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> U'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
REDUCE'II'IN2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF)
TAUTOLOGY'I'IN1(F) -> U'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 18 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN2(cons2(X0, Xs), Ys) -> INTERSECT'II'IN2(Xs, Ys)
INTERSECT'II'IN2(Xs, cons2(X0, Ys)) -> INTERSECT'II'IN2(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


INTERSECT'II'IN2(cons2(X0, Xs), Ys) -> INTERSECT'II'IN2(Xs, Ys)
INTERSECT'II'IN2(Xs, cons2(X0, Ys)) -> INTERSECT'II'IN2(Xs, Ys)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(INTERSECT'II'IN2(x1, x2)) = 2·x1 + x2   
POL(cons2(x1, x2)) = 1 + 2·x2   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ PisEmptyProof
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(F1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right)))
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> REDUCE'II'IN2(sequent2(cons2(G1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right))
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REDUCE'II'IN2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right)))
REDUCE'II'IN2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> REDUCE'II'IN2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right))
The remaining pairs can at least be oriented weakly.

REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(F1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> REDUCE'II'IN2(sequent2(cons2(G1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)
Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN2(x1, x2)) = x1   
POL(U'12'15(x1, x2, x3, x4, x5)) = x2 + x3 + x4   
POL(U'6'15(x1, x2, x3, x4, x5)) = x2 + x3 + x4   
POL(cons2(x1, x2)) = x1 + x2   
POL(if2(x1, x2)) = x1 + x2   
POL(iff2(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(intersect'ii'in2(x1, x2)) = x1   
POL(intersect'ii'out) = 0   
POL(nil) = 2   
POL(p1(x1)) = 1 + 2·x1   
POL(reduce'ii'in2(x1, x2)) = 0   
POL(reduce'ii'out) = 0   
POL(sequent2(x1, x2)) = x1 + x2   
POL(u'1'11(x1)) = x1   
POL(u'10'11(x1)) = 1 + x1   
POL(u'11'11(x1)) = 1 + x1   
POL(u'12'15(x1, x2, x3, x4, x5)) = 2 + x1 + x2 + x3 + 2·x4 + x5   
POL(u'12'21(x1)) = 2 + 2·x1   
POL(u'13'11(x1)) = 2 + 2·x1   
POL(u'14'11(x1)) = 2   
POL(u'15'11(x1)) = 0   
POL(u'2'11(x1)) = 1 + 2·x1   
POL(u'3'11(x1)) = 1 + 2·x1   
POL(u'4'11(x1)) = 1 + 2·x1   
POL(u'5'11(x1)) = 2 + 2·x1   
POL(u'6'15(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + x3 + 2·x4 + 2·x5   
POL(u'6'21(x1)) = 2 + x1   
POL(u'7'11(x1)) = 1 + x1   
POL(u'8'11(x1)) = 2 + 2·x1   
POL(u'9'11(x1)) = 1 + x1   
POL(x'2a2(x1, x2)) = x1 + x2   
POL(x'2b2(x1, x2)) = x1 + x2   
POL(x'2d1(x1)) = x1   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> REDUCE'II'IN2(sequent2(cons2(G1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(F1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF)
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REDUCE'II'IN2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> REDUCE'II'IN2(sequent2(cons2(G1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(F1, Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF)
The remaining pairs can at least be oriented weakly.

REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)
Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN2(x1, x2)) = x1   
POL(U'12'15(x1, x2, x3, x4, x5)) = x2 + 2·x3 + x4   
POL(U'6'15(x1, x2, x3, x4, x5)) = x2 + x3 + x4   
POL(cons2(x1, x2)) = x1 + x2   
POL(if2(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(iff2(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(intersect'ii'in2(x1, x2)) = 0   
POL(intersect'ii'out) = 0   
POL(nil) = 2   
POL(p1(x1)) = 1 + 2·x1   
POL(reduce'ii'in2(x1, x2)) = x2   
POL(reduce'ii'out) = 0   
POL(sequent2(x1, x2)) = x1 + x2   
POL(u'1'11(x1)) = 2   
POL(u'10'11(x1)) = 0   
POL(u'11'11(x1)) = 2 + x1   
POL(u'12'15(x1, x2, x3, x4, x5)) = 2 + 2·x1 + 2·x2 + x3 + 2·x4 + 2·x5   
POL(u'12'21(x1)) = 2 + 2·x1   
POL(u'13'11(x1)) = 2   
POL(u'14'11(x1)) = 1 + 2·x1   
POL(u'15'11(x1)) = 0   
POL(u'2'11(x1)) = 2 + x1   
POL(u'3'11(x1)) = 2 + x1   
POL(u'4'11(x1)) = 2   
POL(u'5'11(x1)) = 2   
POL(u'6'15(x1, x2, x3, x4, x5)) = 1 + x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5   
POL(u'6'21(x1)) = 2 + 2·x1   
POL(u'7'11(x1)) = 2 + 2·x1   
POL(u'8'11(x1)) = 2 + x1   
POL(u'9'11(x1)) = 0   
POL(x'2a2(x1, x2)) = x1 + 2·x2   
POL(x'2b2(x1, x2)) = x1 + 2·x2   
POL(x'2d1(x1)) = 1 + 2·x1   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, Gs)), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> U'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
The remaining pairs can at least be oriented weakly.

REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)
Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN2(x1, x2)) = 1 + x1   
POL(U'12'15(x1, x2, x3, x4, x5)) = 2 + x3 + x4   
POL(U'6'15(x1, x2, x3, x4, x5)) = 1 + x4   
POL(cons2(x1, x2)) = 1 + x1 + x2   
POL(if2(x1, x2)) = 2 + x1 + x2   
POL(iff2(x1, x2)) = 2 + 2·x1 + x2   
POL(intersect'ii'in2(x1, x2)) = 0   
POL(intersect'ii'out) = 0   
POL(nil) = 2   
POL(p1(x1)) = 1 + x1   
POL(reduce'ii'in2(x1, x2)) = 2·x2   
POL(reduce'ii'out) = 0   
POL(sequent2(x1, x2)) = x2   
POL(u'1'11(x1)) = 2 + 2·x1   
POL(u'10'11(x1)) = 2   
POL(u'11'11(x1)) = 2   
POL(u'12'15(x1, x2, x3, x4, x5)) = 1 + x2 + 2·x3 + 2·x4 + 2·x5   
POL(u'12'21(x1)) = 2 + 2·x1   
POL(u'13'11(x1)) = 1   
POL(u'14'11(x1)) = 2 + x1   
POL(u'15'11(x1)) = 2 + 2·x1   
POL(u'2'11(x1)) = 2 + 2·x1   
POL(u'3'11(x1)) = 2 + x1   
POL(u'4'11(x1)) = 2   
POL(u'5'11(x1)) = 2   
POL(u'6'15(x1, x2, x3, x4, x5)) = 2 + 2·x1 + 2·x2 + x3 + x4 + 2·x5   
POL(u'6'21(x1)) = 2·x1   
POL(u'7'11(x1)) = 2   
POL(u'8'11(x1)) = 2 + 2·x1   
POL(u'9'11(x1)) = 2 + x1   
POL(x'2a2(x1, x2)) = 1 + x1 + 2·x2   
POL(x'2b2(x1, x2)) = 1 + x1 + x2   
POL(x'2d1(x1)) = 1 + 2·x1   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
QDP
                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
U'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ DependencyGraphProof
QDP
                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> U'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
REDUCE'II'IN2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF)
The remaining pairs can at least be oriented weakly.

U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN2(x1, x2)) = 2 + x1   
POL(U'6'15(x1, x2, x3, x4, x5)) = 2 + 2·x2   
POL(cons2(x1, x2)) = x1   
POL(if2(x1, x2)) = 1 + x1 + x2   
POL(iff2(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(intersect'ii'in2(x1, x2)) = 1 + x1 + 2·x2   
POL(intersect'ii'out) = 0   
POL(nil) = 1   
POL(p1(x1)) = 1   
POL(reduce'ii'in2(x1, x2)) = 1   
POL(reduce'ii'out) = 0   
POL(sequent2(x1, x2)) = 2·x1   
POL(u'1'11(x1)) = 0   
POL(u'10'11(x1)) = 2 + x1   
POL(u'11'11(x1)) = 2   
POL(u'12'15(x1, x2, x3, x4, x5)) = 1 + x1 + x2 + 2·x3 + x4 + 2·x5   
POL(u'12'21(x1)) = 2 + 2·x1   
POL(u'13'11(x1)) = 2   
POL(u'14'11(x1)) = 1   
POL(u'15'11(x1)) = 1   
POL(u'2'11(x1)) = 1   
POL(u'3'11(x1)) = 2 + x1   
POL(u'4'11(x1)) = 2 + 2·x1   
POL(u'5'11(x1)) = 1 + 2·x1   
POL(u'6'15(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + 2·x3 + x4 + 2·x5   
POL(u'6'21(x1)) = 1 + 2·x1   
POL(u'7'11(x1)) = 2   
POL(u'8'11(x1)) = 2   
POL(u'9'11(x1)) = 0   
POL(x'2a2(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(x'2b2(x1, x2)) = 1 + 2·x1 + x2   
POL(x'2d1(x1)) = 2 + 2·x1   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ QDPOrderProof
QDP
                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN2(sequent2(cons2(F2, Fs), Gs), NF)
REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ DependencyGraphProof
QDP
                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)

The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


REDUCE'II'IN2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> REDUCE'II'IN2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN2(x1, x2)) = 2·x1   
POL(cons2(x1, x2)) = 1 + x1   
POL(sequent2(x1, x2)) = x2   
POL(x'2b2(x1, x2)) = 1 + 2·x1 + 2·x2   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ QDPOrderProof
                  ↳ QDP
                    ↳ QDPOrderProof
                      ↳ QDP
                        ↳ DependencyGraphProof
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP
                                    ↳ QDPOrderProof
QDP
                                        ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in2(cons2(X, X0), cons2(X, X1)) -> intersect'ii'out
intersect'ii'in2(Xs, cons2(X0, Ys)) -> u'1'11(intersect'ii'in2(Xs, Ys))
u'1'11(intersect'ii'out) -> intersect'ii'out
intersect'ii'in2(cons2(X0, Xs), Ys) -> u'2'11(intersect'ii'in2(Xs, Ys))
u'2'11(intersect'ii'out) -> intersect'ii'out
reduce'ii'in2(sequent2(cons2(if2(A, B), Fs), Gs), NF) -> u'3'11(reduce'ii'in2(sequent2(cons2(x'2b2(x'2d1(B), A), Fs), Gs), NF))
u'3'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(iff2(A, B), Fs), Gs), NF) -> u'4'11(reduce'ii'in2(sequent2(cons2(x'2a2(if2(A, B), if2(B, A)), Fs), Gs), NF))
u'4'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2a2(F1, F2), Fs), Gs), NF) -> u'5'11(reduce'ii'in2(sequent2(cons2(F1, cons2(F2, Fs)), Gs), NF))
u'5'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2b2(F1, F2), Fs), Gs), NF) -> u'6'15(reduce'ii'in2(sequent2(cons2(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'15(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'21(reduce'ii'in2(sequent2(cons2(F2, Fs), Gs), NF))
u'6'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(x'2d1(F1), Fs), Gs), NF) -> u'7'11(reduce'ii'in2(sequent2(Fs, cons2(F1, Gs)), NF))
u'7'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(if2(A, B), Gs)), NF) -> u'8'11(reduce'ii'in2(sequent2(Fs, cons2(x'2b2(x'2d1(B), A), Gs)), NF))
u'8'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(iff2(A, B), Gs)), NF) -> u'9'11(reduce'ii'in2(sequent2(Fs, cons2(x'2a2(if2(A, B), if2(B, A)), Gs)), NF))
u'9'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(cons2(p1(V), Fs), Gs), sequent2(Left, Right)) -> u'10'11(reduce'ii'in2(sequent2(Fs, Gs), sequent2(cons2(p1(V), Left), Right)))
u'10'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2b2(G1, G2), Gs)), NF) -> u'11'11(reduce'ii'in2(sequent2(Fs, cons2(G1, cons2(G2, Gs))), NF))
u'11'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2a2(G1, G2), Gs)), NF) -> u'12'15(reduce'ii'in2(sequent2(Fs, cons2(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'15(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'21(reduce'ii'in2(sequent2(Fs, cons2(G2, Gs)), NF))
u'12'21(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(Fs, cons2(x'2d1(G1), Gs)), NF) -> u'13'11(reduce'ii'in2(sequent2(cons2(G1, Fs), Gs), NF))
u'13'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, cons2(p1(V), Gs)), sequent2(Left, Right)) -> u'14'11(reduce'ii'in2(sequent2(nil, Gs), sequent2(Left, cons2(p1(V), Right))))
u'14'11(reduce'ii'out) -> reduce'ii'out
reduce'ii'in2(sequent2(nil, nil), sequent2(F1, F2)) -> u'15'11(intersect'ii'in2(F1, F2))
u'15'11(intersect'ii'out) -> reduce'ii'out
tautology'i'in1(F) -> u'16'11(reduce'ii'in2(sequent2(nil, cons2(F, nil)), sequent2(nil, nil)))
u'16'11(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.